Termination Proof Script

Consider the TRS R consisting of the rewrite rules


1:	active(2nd(cons1(X,cons(Y,Z))))	→ mark(Y)
2:	active(2nd(cons(X,X1)))	→ mark(2nd(cons1(X,X1)))
3:	active(from(X))	→ mark(cons(X,from(s(X))))
4:	active(2nd(X))	→ 2nd(active(X))
5:	active(cons(X1,X2))	→ cons(active(X1),X2)
6:	active(from(X))	→ from(active(X))
7:	active(s(X))	→ s(active(X))
8:	active(cons1(X1,X2))	→ cons1(active(X1),X2)
9:	active(cons1(X1,X2))	→ cons1(X1,active(X2))
10:	2nd(mark(X))	→ mark(2nd(X))
11:	cons(mark(X1),X2)	→ mark(cons(X1,X2))
12:	from(mark(X))	→ mark(from(X))
13:	s(mark(X))	→ mark(s(X))
14:	cons1(mark(X1),X2)	→ mark(cons1(X1,X2))
15:	cons1(X1,mark(X2))	→ mark(cons1(X1,X2))
16:	proper(2nd(X))	→ 2nd(proper(X))
17:	proper(cons(X1,X2))	→ cons(proper(X1),proper(X2))
18:	proper(from(X))	→ from(proper(X))
19:	proper(s(X))	→ s(proper(X))
20:	proper(cons1(X1,X2))	→ cons1(proper(X1),proper(X2))
21:	2nd(ok(X))	→ ok(2nd(X))
22:	cons(ok(X1),ok(X2))	→ ok(cons(X1,X2))
23:	from(ok(X))	→ ok(from(X))
24:	s(ok(X))	→ ok(s(X))
25:	cons1(ok(X1),ok(X2))	→ ok(cons1(X1,X2))
26:	top(mark(X))	→ top(proper(X))
27:	top(ok(X))	→ top(active(X))

There are 44 dependency pairs:


28:	ACTIVE(2nd(cons(X,X1)))	→ 2nd#(cons1(X,X1))
29:	ACTIVE(2nd(cons(X,X1)))	→ CONS1(X,X1)
30:	ACTIVE(from(X))	→ CONS(X,from(s(X)))
31:	ACTIVE(from(X))	→ FROM(s(X))
32:	ACTIVE(from(X))	→ S(X)
33:	ACTIVE(2nd(X))	→ 2nd#(active(X))
34:	ACTIVE(2nd(X))	→ ACTIVE(X)
35:	ACTIVE(cons(X1,X2))	→ CONS(active(X1),X2)
36:	ACTIVE(cons(X1,X2))	→ ACTIVE(X1)
37:	ACTIVE(from(X))	→ FROM(active(X))
38:	ACTIVE(from(X))	→ ACTIVE(X)
39:	ACTIVE(s(X))	→ S(active(X))
40:	ACTIVE(s(X))	→ ACTIVE(X)
41:	ACTIVE(cons1(X1,X2))	→ CONS1(active(X1),X2)
42:	ACTIVE(cons1(X1,X2))	→ ACTIVE(X1)
43:	ACTIVE(cons1(X1,X2))	→ CONS1(X1,active(X2))
44:	ACTIVE(cons1(X1,X2))	→ ACTIVE(X2)
45:	2nd#(mark(X))	→ 2nd#(X)
46:	CONS(mark(X1),X2)	→ CONS(X1,X2)
47:	FROM(mark(X))	→ FROM(X)
48:	S(mark(X))	→ S(X)
49:	CONS1(mark(X1),X2)	→ CONS1(X1,X2)
50:	CONS1(X1,mark(X2))	→ CONS1(X1,X2)
51:	PROPER(2nd(X))	→ 2nd#(proper(X))
52:	PROPER(2nd(X))	→ PROPER(X)
53:	PROPER(cons(X1,X2))	→ CONS(proper(X1),proper(X2))
54:	PROPER(cons(X1,X2))	→ PROPER(X1)
55:	PROPER(cons(X1,X2))	→ PROPER(X2)
56:	PROPER(from(X))	→ FROM(proper(X))
57:	PROPER(from(X))	→ PROPER(X)
58:	PROPER(s(X))	→ S(proper(X))
59:	PROPER(s(X))	→ PROPER(X)
60:	PROPER(cons1(X1,X2))	→ CONS1(proper(X1),proper(X2))
61:	PROPER(cons1(X1,X2))	→ PROPER(X1)
62:	PROPER(cons1(X1,X2))	→ PROPER(X2)
63:	2nd#(ok(X))	→ 2nd#(X)
64:	CONS(ok(X1),ok(X2))	→ CONS(X1,X2)
65:	FROM(ok(X))	→ FROM(X)
66:	S(ok(X))	→ S(X)
67:	CONS1(ok(X1),ok(X2))	→ CONS1(X1,X2)
68:	TOP(mark(X))	→ TOP(proper(X))
69:	TOP(mark(X))	→ PROPER(X)
70:	TOP(ok(X))	→ TOP(active(X))
71:	TOP(ok(X))	→ ACTIVE(X)

The approximated dependency graph contains 8 SCCs: {45,63}, {46,64}, {49,50,67}, {47,65}, {48,66}, {52,54,55,57,59,61,62}, {34,36,38,40,42,44} and {68,70}.

Consider the SCC {45,63}. There are no usable rules. By taking the AF π with π(2nd#) = π(mark) = 1 together with the lexicographic path order with empty precedence, rule 45 is weakly decreasing and rule 63 is strictly decreasing. There is one new SCC.
- Consider the SCC {45}. By taking the AF π with π(2nd#) = 1 together with the lexicographic path order with empty precedence, rule 45 is strictly decreasing.

Consider the SCC {46,64}. There are no usable rules. By taking the AF π with π(CONS) = π(mark) = 1 together with the lexicographic path order with empty precedence, rule 46 is weakly decreasing and rule 64 is strictly decreasing. There is one new SCC.
- Consider the SCC {46}. By taking the AF π with π(CONS) = 1 together with the lexicographic path order with empty precedence, rule 46 is strictly decreasing.

Consider the SCC {49,50,67}. There are no usable rules. By taking the AF π with π(CONS1) = π(mark) = 1 together with the lexicographic path order with empty precedence, the rules in {49,50} are weakly decreasing and rule 67 is strictly decreasing. There is one new SCC.
- Consider the SCC {49,50}. By taking the AF π with π(CONS1) = 1 together with the lexicographic path order with empty precedence, rule 50 is weakly decreasing and rule 49 is strictly decreasing. There is one new SCC.
  - Consider the SCC {50}. By taking the AF π with π(CONS1) = 2 together with the lexicographic path order with empty precedence, rule 50 is strictly decreasing.

Consider the SCC {47,65}. There are no usable rules. By taking the AF π with π(FROM) = π(mark) = 1 together with the lexicographic path order with empty precedence, rule 47 is weakly decreasing and rule 65 is strictly decreasing. There is one new SCC.
- Consider the SCC {47}. By taking the AF π with π(FROM) = 1 together with the lexicographic path order with empty precedence, rule 47 is strictly decreasing.

Consider the SCC {48,66}. There are no usable rules. By taking the AF π with π(mark) = π(S) = 1 together with the lexicographic path order with empty precedence, rule 48 is weakly decreasing and rule 66 is strictly decreasing. There is one new SCC.
- Consider the SCC {48}. By taking the AF π with π(S) = 1 together with the lexicographic path order with empty precedence, rule 48 is strictly decreasing.

Consider the SCC {52,54,55,57,59,61,62}. There are no usable rules. By taking the AF π with π(2nd) = π(from) = π(PROPER) = π(s) = 1 together with the lexicographic path order with empty precedence, the rules in {52,57,59} are weakly decreasing and the rules in {54,55,61,62} are strictly decreasing. There is one new SCC.
- Consider the SCC {52,57,59}. By taking the AF π with π(2nd) = π(from) = π(PROPER) = 1 together with the lexicographic path order with empty precedence, the rules in {52,57} are weakly decreasing and rule 59 is strictly decreasing. There is one new SCC.
  - Consider the SCC {52,57}. By taking the AF π with π(2nd) = π(PROPER) = 1 together with the lexicographic path order with empty precedence, rule 52 is weakly decreasing and rule 57 is strictly decreasing. There is one new SCC.
    - Consider the SCC {52}. By taking the AF π with π(PROPER) = 1 together with the lexicographic path order with empty precedence, rule 52 is strictly decreasing.

Consider the SCC {34,36,38,40,42,44}. There are no usable rules. By taking the AF π with π(2nd) = π(ACTIVE) = π(cons) = π(from) = π(s) = 1 together with the lexicographic path order with empty precedence, the rules in {34,36,38,40} are weakly decreasing and the rules in {42,44} are strictly decreasing. There is one new SCC.
- Consider the SCC {34,36,38,40}. By taking the AF π with π(2nd) = π(ACTIVE) = π(cons) = π(from) = 1 together with the lexicographic path order with empty precedence, the rules in {34,36,38} are weakly decreasing and rule 40 is strictly decreasing. There is one new SCC.
  - Consider the SCC {34,36,38}. By taking the AF π with π(2nd) = π(ACTIVE) = π(cons) = 1 together with the lexicographic path order with empty precedence, the rules in {34,36} are weakly decreasing and rule 38 is strictly decreasing. There is one new SCC.
    - Consider the SCC {34,36}. By taking the AF π with π(2nd) = π(ACTIVE) = 1 and π(cons) = [1] together with the lexicographic path order with empty precedence, rule 34 is weakly decreasing and rule 36 is strictly decreasing. There is one new SCC.
      - Consider the SCC {34}. By taking the AF π with π(ACTIVE) = 1 together with the lexicographic path order with empty precedence, rule 34 is strictly decreasing.

Consider the SCC {68,70}. The usable rules are {1-25}. The constraints could not be solved.

Tyrolean Termination Tool (37.35 seconds) --- May 3, 2006